$\forall$${\it da}$:$k$:Knd fp$\rightarrow$ Type. Msg(${\it da}$) $\in$ Type